In this tutorial we give a short introduction to the usage of the main
functionalities of \nusmv. 
In \cref{Examples} we describe the input language of \nusmv by
presenting some examples of \nusmv models.
\cref{Simulation} shows how the user can get familiar with the behavior
of a \nusmv model by exploring its possible executions.
\cref{CTL Model Checking} and \cref{LTL Model Checking} give an overview
of BDD-based model checking, while \cref{Bounded Model Checking} presents
SAT-based model checking in \nusmv.
